Nuprl Lemma : alle-at2_wf
0,22
postcript
pdf
es
:ES,
i
,
x
,
y
:Id,
P
:(vartype(
i
;
x
)
vartype(
i
;
y
)
Prop). @
i
always.
P
(
v1
,
v2
)
Prop
latex
Definitions
x
:
A
.
B
(
x
)
,
vartype(
i
;
x
)
,
t
T
,
x
when
e
,
ES
,
Id
,
Prop
,
loc(
e
)
,
E
,
x
(
s1
,
s2
)
,
x
.
t
(
x
)
,
e
@
i
.
P
(
e
)
,
@
i
always.
P
(
x1
;
x2
)
Lemmas
alle-at
wf
,
es-E
wf
,
es-loc
wf
,
Id
wf
,
event
system
wf
,
es-when
wf
,
es-vartype
wf
origin
es:ES, i, x, y:Id, P:(vartype(i;x)
vartype(i;y)Prop). @i always.P(v1,v2) 
Prop es:ES, i, x, y:Id, P:(vartype(i;x)vartype(i;y)Prop). @i always.P(v1,v2) Prop x:A. B(x) T
x. t(x)e@i. P(e)